Inference at * 1 0 
Iof proof for Lemma trans functionality wrt iff:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. R(x,y)  R'(x,y)
  (a, b, c:T. R(b,a)  R(c,b)  R(c,a))  (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a)) 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{19:n,
 by PERMUTE{20:n,
 by PERMUTE{21:n,
 by PERMUTE{22:n,
 by PERMUTE{23:n,
 by PERMUTE{24:n,
 by PERMUTE{25:n,
 by PERMUTE{19:n,
 by PERMUTE{25:n,
 by PERMUTE{20:n,
 by PERMUTE{11:n,
 by PERMUTE{7:n,
 by PERMUTE{3:n,
 by PERMUTE{26:n,
 by PERMUTE{27:n} 

latex

 1: .....wf..... NILNIL

 1:   (a, b, c:T. R(b,a)  R(c,b)  R(c,a))  
 2: .....wf..... NILNIL

 2:   (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a))  
 3: .....wf..... NILNIL

 3:   T  Type
 4: .....wf..... NILNIL

 4:   (a.b, c:T. R(b,a)  R(c,b)  R(c,a))  T
 5: .....wf..... NILNIL

 5:   (a.b, c:T. R'(b,a)  R'(c,b)  R'(c,a))  T
 6: .....wf..... NILNIL

 6:   T = T
 7: .....wf..... NILNIL

 7: 5. T
 7:   T  Type
 8: .....wf..... NILNIL

 8: 5. a : T
 8:   (b.c:T. R(b,a)  R(c,b)  R(c,a))  T
 9: .....wf..... NILNIL

 9: 5. a : T
 9:   (b.c:T. R'(b,a)  R'(c,b)  R'(c,a))  T
 10: .....wf..... NILNIL

 10: 5. T
 10:   T = T
 11: .....wf..... NILNIL

 11: 5. T
 11: 6. T
 11:   T  Type
 12: .....wf..... NILNIL

 12: 5. a : T
 12: 6. b : T
 12:   (c.R(b,a)  R(c,b)  R(c,a))  T
 13: .....wf..... NILNIL

 13: 5. a : T
 13: 6. b : T
 13:   (c.R'(b,a)  R'(c,b)  R'(c,a))  T
 14: .....wf..... NILNIL

 14: 5. T
 14: 6. T
 14:   T = T
 15: .....wf..... NILNIL

 15: 5. a : T
 15: 6. b : T
 15: 7. T
 15:   R(b,a)  
 16: .....wf..... NILNIL

 16: 5. a : T
 16: 6. b : T
 16: 7. T
 16:   R'(b,a)  
 17: .....wf..... NILNIL

 17: 5. a : T
 17: 6. b : T
 17: 7. c : T
 17:   (R(c,b)  R(c,a))  
 18: .....wf..... NILNIL

 18: 5. a : T
 18: 6. b : T
 18: 7. c : T
 18:   (R'(c,b)  R'(c,a))  
 19: .....wf..... NILNIL

 19: 5. T
 19: 6. b : T
 19: 7. T
 19:   b  T
 20: .....wf..... NILNIL

 20: 5. a : T
 20: 6. T
 20: 7. T
 20:   a  T
 21: .....wf..... NILNIL

 21: 5. T
 21: 6. b : T
 21: 7. c : T
 21:   R(c,b)  
 22: .....wf..... NILNIL

 22: 5. T
 22: 6. b : T
 22: 7. c : T
 22:   R'(c,b)  
 23: .....wf..... NILNIL

 23: 5. a : T
 23: 6. T
 23: 7. c : T
 23:   R(c,a)  
 24: .....wf..... NILNIL

 24: 5. a : T
 24: 6. T
 24: 7. c : T
 24:   R'(c,a)  
 25: .....wf..... NILNIL

 25: 5. T
 25: 6. T
 25: 7. c : T
 25:   c  T
 26: .....wf..... NILNIL

 26:   (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a)) = (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a))
 27: 

 27:   (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a))  (a, b, c:T. R'(b,a)  R'(c,b)  R'(c,a))
 .

Definitions	t  T, x:A  B(x), x.A(x), f(a), s = t, x(s1,s2), , x:AB(x), Type, {T}, x(s), P & Q, x. t(x), P  Q, P  Q, P  Q, x:A. B(x)
Lemmas	implies functionality wrt iff, all functionality wrt iff, iff functionality wrt iff